package iset.coverageanalyzer.instrument;

import iset.coverageanalyzer.config.ConfigInfo;
import iset.coverageanalyzer.data.CoverageInfo;

import java.io.BufferedReader;
import java.io.FileInputStream;
import java.io.IOException;
import java.io.InputStreamReader;
import java.io.PrintWriter;
import java.util.ArrayList;
import java.util.List;

public class JavaInstrumentor {
	
	private CoverageInfo coverageInfo = null;
	
	public JavaInstrumentor(){
		
	}
	
	public JavaInstrumentor(CoverageInfo coverageInfo){
		this.coverageInfo = coverageInfo;
	}
	
	public void setCoverageInfo(CoverageInfo coverageInfo){
		this.coverageInfo = coverageInfo;
	}
	
	/**
	 * 
	 * This method can only be used in the method with one return statement or zero return statement.
	 * 
	 * @return
	 * @throws IOException
	 */
	public int instrument() throws IOException{
		
		String srcFile = coverageInfo.configInfo.inputJava;
		String dstFile = coverageInfo.configInfo.outputJava;
		
		String dstJPFFile = coverageInfo.configInfo.outputJPF;
		
		BufferedReader br = new BufferedReader(new InputStreamReader( new FileInputStream(srcFile)));
		List<String> srcLines = new ArrayList<String>();
		String oneLine = null;
		
		int lastMeaningLine = -1;
		int tmpCount = 0;
		while( (oneLine = br.readLine())!= null){
			tmpCount++;
			srcLines.add(oneLine);
			if((tmpCount >= this.coverageInfo.method_startLineNum) && (tmpCount <= this.coverageInfo.method_endLineNum)){
				if( oneLine.trim().startsWith("return")){
					lastMeaningLine = srcLines.size();
				}
			}
		}
		br.close();
		
		int lineNum = coverageInfo.lineNum;
		int method_start = coverageInfo.method_startLineNum;
		int method_end = coverageInfo.method_endLineNum;
		List<String> dstLines = new ArrayList<String>();
		
		String packageInfo = getPackageInfo(srcLines);
		dstLines.add(packageInfo);
		dstLines.add("import gov.nasa.jpf.jvm.Verify;");
		dstLines.add("import gov.nasa.jpf.symbc.Debug;");
		dstLines.add("\n");
		
		
		
		for(int i=0;i<srcLines.size();i++){		
			
			if(srcLines.get(i).startsWith("package")){
				continue;
			}
			
			if( i == (method_start-1)){
				dstLines.add("boolean flag = false;  // this code is generated by Jabolic, do not edit this!");
			}
			
			if(i== (lineNum-1)){
				dstLines.add("flag = true; // this code is generated by Jabolic, do not edit this!");
			}
			
			if( i == (lastMeaningLine-1)){
				dstLines.add("Verify.ignoreIf(!flag); // this code is generated by Jabolic, do not edit this!");
			}
			
			
			
			dstLines.add(srcLines.get(i));
		
			if( i == (method_end-1)){
				if(lastMeaningLine == -1){
					dstLines.add("Verify.ignoreIf(!flag); // this code is generated by Jabolic, do not edit this!");
				}
			}
		}
		
		// check the last location of char '}' 
		int lastLine = -1;
		boolean formatFlag = true;
		for(int i=dstLines.size()-1;i>=0;i--){
			
			if(dstLines.get(i).trim().equalsIgnoreCase("}")){
				lastLine = i;
				break;
			}
			
			if(dstLines.get(i).trim().equalsIgnoreCase("")){
				formatFlag = true;
			}else{
				formatFlag = false;
				if(lastLine == -1){
					lastLine = i;
				}
			}
		}
		
		PrintWriter pw = new PrintWriter(dstFile);
		for(int i=0;i<dstLines.size();i++){
			// if the last line meets, add the auto generated code here, a main function
			if((i == lastLine)){
				pw.println(autoGeneratedCode());
			}
			pw.println(dstLines.get(i));
		}
		
		pw.flush();
		pw.close();
		
		return InstrumentResult.SUCCESS;
	}
	
	public String autoGeneratedCode(){
		StringBuffer sb = new StringBuffer();
		sb.append("/*  \r\n");
		sb.append(" *  automatically added by Jabolic tester, plz edit yourself according to the project to be test!\r\n");
		sb.append(" */ \r\n");
		sb.append(" public static void main(String[] args){ \r\n");
		sb.append(" \t/* \r\n"+
		 " \t* fill in an initial test case for one method, \r\n"+
		 " \t* It should corresponds to one of the test method in corresponding JUnit Test class \r\n"+
		 " \t* An example: foo.bar(p1, p2,...); \r\n"+
		 " \t* the corresponder: testBar(p1, p2,...); \r\n"+
		 " \t*/ \r\n");
		sb.append(" \tDebug.printPC(\"\\nSc.add Path Condition: \");\r\n");
		sb.append(" \t}");
		return sb.toString();
	}
	
	public String getPackageInfo(List<String> lines){
		String temp = null;
		for(int i=0;i<lines.size();i++){
			temp = lines.get(i);
			if(temp.startsWith("package")){
				return temp;
			}else if(temp.startsWith("import")){
				return "";
			}
		}
		return "";
	}
	
	public static void main(String[] args){
		
		ConfigInfo config = new ConfigInfo();
		config.inputJava = "JustTest.java";
		config.outputJava = "JustTest_instrumented.java";
		CoverageInfo ci = new CoverageInfo( config );
		ci.className = "JustTest";
		ci.lineNum = 7;
		
		JavaInstrumentor ji = new JavaInstrumentor(ci);
		try {
			ji.instrument();
		} catch (IOException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}
	}
}
